-- Types

type byte = bits(8)
type word = bits(32)
type addr = bits(32)
type mem = addrT -> byteT
type reg = bits(4)

-- Registers

register PSR :: word
{
     31 : N
     30 : Z
     29 : C
     28 : V
  27- 9 : RAZ!
      8 : A
      7 : I
      6 : F
      5 : RAZ! -- Thumb mode
   4- 0 : Mode
}

-- State

declare
{
  pc :: addr
  gpr :: reg -> word
  mem :: mem
  CPSR :: PSR
  SPSR_fiq :: PSR
  SPSR_irq :: PSR
  SPSR_svc :: PSR
  SPSR_abt :: PSR
  SPSR_und :: PSR
}

-- GPR access

component R (n::reg) :: word
{
  value = gpr(n)
  assign value = gpr(n) <- value
}

bits(N) * bool * bool
AddWithCarry (x::bits(N), y::bits(N), carry_in::bool) =
{
  unsigned_sum = [x] + [y] + [carry_in] :: nat;
  signed_sum = [x] + [y] + [carry_in] :: int;
  result = [unsigned_sum]::bits(N);
  carry_out = [result] != unsigned_sum;
  overflow = [result] != signed_sum;
  return result, carry_out, overflow
}

word * bool * bool
DataProcessingALU (op::bits(4), a::word, b::word, c::bool) =
  match op
  {
    case '0000' or '1000' => a && b, c, UNKNOWN          -- AND, TST
    case '0001' or '1001' => a ?? b, c, UNKNOWN          -- EOR, TEQ
    case '0010' or '1010' => AddWithCarry (a, ~b, true)  -- SUB, CMP
    case '0011'           => AddWithCarry (~a, b, true)  -- RSB
    case '0100' or '1011' => AddWithCarry (a, b, false)  -- ADD, CMN
    case '0101'           => AddWithCarry (a, b, c)      -- ADC
    case '0110'           => AddWithCarry (a, ~b, c)     -- SBC
    case '0111'           => AddWithCarry (~a, b, c)     -- RSC
    case '1100'           => a || b, c, UNKNOWN          -- ORR
    case '1101'           => b, c, UNKNOWN               -- MOV
    case '1110'           => a && ~b, c, UNKNOWN         -- BIC
    case '1111'           => ~b, c, UNKNOWN              -- MVN
  }

bool ArithmeticOpcode (op::bits(4)) =
  (op<2> or op<1>) and not (op<3> and op<2>)

unit DataProcessing
  ( op :: bits(4),
    S :: bool,
    d :: reg,
    n :: reg,
    imm32 :: word,
    C :: bool ) =
{
  rn = R(n);

  result, carry, overflow = DataProcessingALU (op, rn, imm32, CPSR.C);

  when op<3:2> != 0b10 do
    R(d) <- result;

  when S do
  {
    CPSR.N <- result<31>;
    CPSR.Z <- result == 0;
    if ArithmeticOpcode (op) then
    {
       CPSR.C <- carry;
       CPSR.V <- overflow
    }
    else
      CPSR.C <- C
  }
}
